Telegram Group & Telegram Channel
✔️ А вот и новый DeepSeek Prover v2, модель, заточенная исключительно на математику.

🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).

Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.

Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.

Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.

Результаты:
Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.

Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.

🔍 Как это работает:

1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.

2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.

3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.

🌟 Два размера:
7 B — базовый вариант.
671 B — расширенная версия на базе DeepSeek-V3-Base.

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
Please open Telegram to view this post
VIEW IN TELEGRAM



tg-me.com/sqlhub/1867
Create:
Last Update:

✔️ А вот и новый DeepSeek Prover v2, модель, заточенная исключительно на математику.

🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).

Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.

Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.

Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.

Результаты:
Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.

Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.

🔍 Как это работает:

1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.

2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.

3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.

🌟 Два размера:
7 B — базовый вариант.
671 B — расширенная версия на базе DeepSeek-V3-Base.

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

BY Data Science. SQL hub




Share with your friend now:
tg-me.com/sqlhub/1867

View MORE
Open in Telegram


Data Science SQL hub Telegram | DID YOU KNOW?

Date: |

Telegram has exploded as a hub for cybercriminals looking to buy, sell and share stolen data and hacking tools, new research shows, as the messaging app emerges as an alternative to the dark web.An investigation by cyber intelligence group Cyberint, together with the Financial Times, found a ballooning network of hackers sharing data leaks on the popular messaging platform, sometimes in channels with tens of thousands of subscribers, lured by its ease of use and light-touch moderation.

The lead from Wall Street offers little clarity as the major averages opened lower on Friday and then bounced back and forth across the unchanged line, finally finishing mixed and little changed.The Dow added 33.18 points or 0.10 percent to finish at 34,798.00, while the NASDAQ eased 4.54 points or 0.03 percent to close at 15,047.70 and the S&P 500 rose 6.50 points or 0.15 percent to end at 4,455.48. For the week, the Dow rose 0.6 percent, the NASDAQ added 0.1 percent and the S&P gained 0.5 percent.The lackluster performance on Wall Street came on uncertainty about the outlook for the markets following recent volatility.

Data Science SQL hub from ua


Telegram Data Science. SQL hub
FROM USA